DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2022.12

Type-Based Termination for Futures

Authors: Siva Somayyajula and Frank Pfenning

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract

In sequential functional languages, sized types enable termination checking of programs with complex patterns of recursion in the presence of mixed inductive-coinductive types. In this paper, we adapt sized types and their metatheory to the concurrent setting. We extend the semi-axiomatic sequent calculus, a subsuming paradigm for futures-based functional concurrency, and its underlying operational semantics with recursion and arithmetic refinements. The latter enables a new and highly general sized type scheme we call sized type refinements. As a widely applicable technical device, we type recursive programs with infinitely deep typing derivations that unfold all recursive calls. Then, we observe that certain such derivations can be made infinitely wide but finitely deep. The resulting trees serve as the induction target of our strong normalization result, which we develop via a novel logical relations argument.

Cite as

Siva Somayyajula and Frank Pfenning. Type-Based Termination for Futures. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 12:1-12:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{somayyajula_et_al:LIPIcs.FSCD.2022.12,
  author =	{Somayyajula, Siva and Pfenning, Frank},
  title =	{{Type-Based Termination for Futures}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{12:1--12:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.12},
  URN =		{urn:nbn:de:0030-drops-162931},
  doi =		{10.4230/LIPIcs.FSCD.2022.12},
  annote =	{Keywords: type-based termination, sized types, futures, concurrency, infinite proofs}
}

Search Results

Documents authored by Somayyajula, Siva

Type-Based Termination for Futures

Abstract

Cite as

Thanks for your feedback!

Could not send message